$\forall$$A$:Type, $d$:DS($A$), $a$:$A$, $x$, $y$:dstype($A$; $d$; $a$). \{($x$ = $y$) $\Leftarrow\!\Rightarrow$ ($\uparrow$$x$ = $y$)\}